usends1-p(es;ds;k;T;l;tg;B;f)
== ((x:Id. subtype_rel(es-vartype(es; source(l); x); fpf-cap(ds; id-deq; x; top)))
==  alle-at(es; source(l); e.((es-kind(es; e) = k)  subtype_rel(es-valtype(es; e); T)))
==  (e:es-E(es). (es-kind(es; e) = rcv(l,tg))  subtype_rel(es-valtype(es; e); B)))
== c alle-at(es;
== c alle-at(source(l);
== c alle-at(e.((es-kind(es; e) = k)
== c alle-at( (e':es-E(es)
== c alle-at( (((es-kind(es; e') = rcv(l,tg))
== c alle-at( (c ((es-sender(es; e') = e)
== c alle-at( (c  (e'':es-E(es). 
== c alle-at( (c  (es-kind(es; e'') = rcv(l,tg))  (es-sender(es; e'') = e)  (e'' = e'))
== c alle-at( (c  (es-val(es; e') = f(es-state-when(es; e),es-val(es; e)))))))) 

latex

---

clarification:

usends1-p(es;ds;k;T;l;tg;B;f)
== ((x:Id. subtype_rel(es-vartype(es; source(l); x); fpf-cap(ds; id-deq; x; top)))
==  alle-at(es; source(l); e.((es-kind(es; e) = k  Knd)  subtype_rel(es-valtype(es; e); T)))
==  (e:es-E(es). (es-kind(es; e) = rcv(l,tg)  Knd)  subtype_rel(es-valtype(es; e); B)))
== c alle-at(es;
== c alle-at(source(l);
== c alle-at(e.((es-kind(es; e) = k  Knd)
== c alle-at( (e':es-E(es)
== c alle-at( (((es-kind(es; e') = rcv(l,tg)  Knd)
== c alle-at( (c ((es-sender(es; e') = e  es-E(es))
== c alle-at( (c  (e'':es-E(es). 
== c alle-at( (c  (es-kind(es; e'') = rcv(l,tg)  Knd)
== c alle-at( (c   (es-sender(es; e'') = e  es-E(es))
== c alle-at( (c   (e'' = e'  es-E(es)))
== c alle-at( (c  (es-val(es; e') = f(es-state-when(es; e),es-val(es; e))  B)))))) 

latex

Definitions	Id, es-vartype(es; i; x), fpf-cap(f; eq; x; z), id-deq, top, es-valtype(es; e), alle-at(es; i; e.P(e)), source(l), x:A. B(x), A c B, P  Q, x:A. B(x), Knd, es-kind(es; e), rcv(l,tg), P  Q, es-sender(es; e), es-E(es), s = t, f(a), es-state-when(es; e), es-val(es; e)
FDL editor aliases	usends1-p